es:ES, e1:E, e2:{e:E| loc(e) = loc(e1)  Id} ,
p:({e:E| loc(e) = loc(e1)  Id} {e:E| loc(e) = loc(e1)  Id} ).
[e1,e2]~([a,b].p(a,b))+   

latex

Definitions	ES, t  T, x:A. B(x), E, loc(e), Id, , x(s1,s2), x,y. t(x;y), [e1;e2]~([a,b].p(a;b))*[a,b].q(a;b), [e1,e2]~([a,b].p(a;b))+
Lemmas	es-pstar-q wf, Id wf, es-loc wf, es-E wf, event system wf